val-axiom(E;V;M;info;pred?;
init;Trans;
Choose;Send;val;time)
== (e:E. 
== (islocal(kind(e)))
==  (x:
==  (((isl(Choose(loc(e),act(kind(e)),x,x.state_when(e)(x,0))))
==  (c (val(e) = outl(Choose(loc(e),act(kind(e)),x,x.state_when(e)(x,0)))))))
==  (e:E. 
==  (isrcv(kind(e)))
==   (<lnk(kind(e)), tag(kind(e)), val(e)>  Send
==   (<lnk(kind(e)), tag(kind(e)), val(e)>  (loc(sender(e))
==   (<lnk(kind(e)), tag(kind(e)), val(e)>  ,kind(sender(e))
==   (<lnk(kind(e)), tag(kind(e)), val(e)>  ,val(sender(e))
==   (<lnk(kind(e)), tag(kind(e)), val(e)>  ,x.state_when(sender(e))(x,0)))) 

latex

---

clarification:

val-axiom(E;V;M;info;pred?;
init;Trans;
Choose;Send;val;time)
== (e:E. 
== (islocal(kind(info;e)))
==  (x:
==  (((isl(Choose
==  (((isl((loc(info;e)
==  (((isl(,act(kind(info;e))
==  (((isl(,x
==  (((isl(,x.state_when(e;info;pred?;init;Trans;val;time)(x,0))))
==  (c (val(e)
==  (c (=
==  (c (outl(Choose
==  (c (outl((loc(info;e)
==  (c (outl(,act(kind(info;e))
==  (c (outl(,x
==  (c (outl(,x.state_when(e;info;pred?;init;Trans;val;time)(x,0)))
==  (c ( V(loc(info;e),act(kind(info;e)))))))
==  (e:E. 
==  (isrcv(kind(info;e)))
==   (<lnk(kind(info;e))
==   , tag(kind(info;e))
==   , val(e)>  Send
==   , val(e)>  (loc(info;sender(info;e))
==   , val(e)>  ,kind(info;sender(info;e))
==   , val(e)>  ,val(sender(info;e))
==   , val(e)>  ,x.state_when(sender(info;e);info;pred?;init;Trans;val;time)
==   , val(e)>  ,x.(x
==   , val(e)>  ,x.,0))  Msg(M))) 

latex

Definitions	P  Q, islocal(k), x:A. B(x), , A c B, isl(x), s = t, outl(x), act(k), x:A. B(x), P  Q, b, isrcv(k), (x  l), lnk(k), <a, b>, tag(k), loc(e), kind(e), x.A(x), f(a), state_when(e), sender(e), #$n, Msg(M)
FDL editor aliases	val-axiom